n:. {m:| m = fib(n)  }  

latex

ProofTree

Definitions	n+m, fib(n), , s = t, #$n, n - m, , a < b, P  Q, A  B, x:A. B(x), {x:A| B(x)} , t  T, x:AB(x), i  j , Void, False, A, -n, , callbyvalue(a;x.B(x)), has-value(a), f(a), True, T, {T}, SQType(T), s ~ t, left + right, P  Q, Dec(P), (i = j), P & Q, b, b, x:A  B(x), Type, p  q, , p q, P  Q, P  Q, Unit, x.A(x)
Lemmas	eqtt to assert, assert of bor, or functionality wrt iff, eqff to assert, squash wf, true wf, bnot thru bor, assert of band, and functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, bor wf, bool wf, band wf, bnot wf, not wf, assert wf, eq int wf, decidable int equal, fib wf, le wf, ge wf, nat properties, nat wf